$\forall$$S$, $T$:Type, $f$:($S$$\rightarrow$$T$), $b$:$\mathbb{B}$, $p$, $q$:$S$. \\[0ex]$f$(if $b$ then $p$ else $q$ fi ) = if $b$ then $f$($p$) else $f$($q$) fi